T:Type, L:T List, R:({x:T| (x  L) }Realizer), x:T.
(xL. R-Feasible(R(x)))
 (x:T. Dec((x  L)))
 (x, y:T. (x  L)  (y  L)  R(x) || R(y))
 (x  L)
 [[R(x)]]  [[xL.R(x)]] 

latex

Definitions	x:A. B(x), P  Q, xL. P(x), x(s), Top, t  T, S  T, x. t(x), Prop, False, x,y. t(x;y), x:A. B(x), P & Q, {T}, Dec(P), P  Q, A, x(s1,s2), P  Q, P  Q, mapl(f;l), Dsys
Lemmas	R-Dsys-Rall2, top wf, dsys-join-list-property, l member wf, R-compat wf, decidable wf, R-Feasible wf, es realizer wf, map-wf2, dsys wf, R-Dsys wf, pairwise-mapl, m-sys-compatible wf, R-compat-implies, member map, list-subtype, l member-set